Controller synthesis is a theoretical approach to the systematic design of discrete event systems. It constructs a controller to provide feedback and control to the system, ensuring it meets specified control specifications. Traditional controller synthesis methods often use formal languages to describe control specifications and are mainly oriented towards single-agent and non-probabilistic systems. With the increasing complexity of systems, the control requirements that need to be satisfied also become more complex. Based on this, this paper proposes a controller synthesis method for semi-cooperative semi-competitive multi-agent probabilistic discrete event systems to solve the controller synthesis problem based on temporal logic specifications. The controller can ensure the satisfaction of specifications to a certain extent. The specification is given in the form of a linear temporal logic formula. This paper designs a controller synthesis algorithm that combines probabilistic model checking. Finally, the effectiveness of this method is verified through a case study.

In this paper, we consider the problem of probabilistic stability analysis of a subclass of Stochastic Hybrid Systems, namely, Polyhedral Probabilistic Hybrid Systems (PPHS), where the flow dynamics is given by a polyhedral inclusion, the discrete switching between modes happens probabilistically at the boundaries of their invariant regions and the continuous state is not reset during switching. We present an abstraction-based analysis framework that consists of constructing a finite Markov Decision Processes (MDP) such that verification of certain property on the finite MDP ensures the satisfaction of probabilistic stability on the PPHS. Further, we present a polynomial-time algorithm for verifying the corresponding property on the MDP. Our experimental analysis demonstrates the feasibility of the approach in successfully verifying probabilistic stability on PPHS of various dimensions and sizes.

In this paper, we study the probabilistic stability analysis of a subclass of stochastic hybrid systems, called the Planar Probabilistic Piecewise Constant Derivative Systems (Planar PPCD), where the continuous dynamics is deterministic, constant rate and planar, the discrete switching between the modes is probabilistic and happens at boundary of the invariant regions, and the continuous states are not reset during switching. These aptly model piecewise linear behaviors of planar robots. Our main result is an exact algorithm for deciding absolute and almost sure stability of Planar PPCD under some mild assumptions on mutual reachability between the states and the presence of non-zero probability self-loops. Our main idea is to reduce the stability problems on planar PPCD into corresponding problems on Discrete Time Markov Chains with edge weights.

The situation calculus has proved to be a very popular formalism for modeling and reasoning about dynamic systems. This otherwise elegant and refined language however lacks a natural way of dealing with "infinite future histories". To this end, in this paper we introduce a new sort ranging over infinite paths in the situation calculus and propose an axiomatization for infinite paths. We thus obtain a convenient way of specifying several kinds of notions that involve infinite futures such as temporal properties of non-terminating executions of agents or programs and mental attitudes such as desires and intentions. We prove the correctness of the axiomatization and show that our formalization has some intuitively desirable properties.

Linear Temporal Logic (LTL) is widely used for defining conditions on the execution paths of dynamic systems. In the case of dynamic systems that allow for nondeterministic evolutions, one has to specify, along with an LTL formula f, which are the paths that are required to satisfy the formula. Two extreme cases are the universal interpretation A.f, which requires that the formula be satisfied for all execution paths, and the existential interpretation E.f, which requires that the formula be satisfied for some execution path. When LTL is applied to the definition of goals in planning problems on nondeterministic domains, these two extreme cases are too restrictive. It is often impossible to develop plans that achieve the goal in all the nondeterministic evolutions of a system, and it is too weak to require that the goal is satisfied by some execution. In this paper we explore alternative interpretations of an LTL formula that are between these extreme cases. We define a new language that permits an arbitrary combination of the A and E quantifiers, thus allowing, for instance, to require that each finite execution can be extended to an execution satisfying an LTL formula (AE.f), or that there is some finite execution whose extensions all satisfy an LTL formula (EA.f). We show that only eight of these combinations of path quantifiers are relevant, corresponding to an alternation of the quantifiers of length one (A and E), two (AE and EA), three (AEA and EAE), and infinity ((AE)* and (EA)*). We also present a planning algorithm for the new language that is based on an automata-theoretic approach, and study its complexity.